A, B:Realizer.
((Rplus?(A)))
 ((Rplus?(B)))
 R-Feasible(A)
 R-Feasible(B)
 A || B
 [[A]] || [[B]] 

latex

Definitions

ma-frame-compatible(A;B), P & Q, A ||+ B, True, T, @i: A, A || B, A  B, case(R)Rnone: noneleft  right: comb(left;right)base(b). base(b), x. t(x), False, , {T}, SQType(T), t  T, ff, tt, Rnone?(x1), if b then t else f fi , [[R]], b, A, P  Q, x:A. B(x), , x(s), Unit, P  Q, P  Q, Y, A || B, Realizer, left  right, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rnone(),

Lemmas

frame-compatible-R-base-ma-pair, compatible-R-base-ma-pair, frame-compatible-R-base-ma, squash wf, ma-compat weakening, R-base-domain wf, eq bd wf, ma-empty wf, ma-empty-compat-left, R-base-ma wf, ma-empty-compat-right, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, R-Dsys-base, es realizer wf, Rplus? wf, R-Feasible wf, R-compat wf, m-sys-null-compatible-right, not wf, R-size-base, R-Dsys-base-wf, m-sys-null-compatible-left, false wf, true wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf, Rnone? wf, assert of bnot, eqff to assert, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, bool sq, bool cases